\subsection{Model-Checking Algebraic Petri Nets with \Alpina}
\label{sec:Alpina}

\Alpina (Algebraic Petri Net Analyzer) is a model-checker developed by the \textsc{Smv} team in Geneva \cite{J:Hostettler-etAl:2011}. \Alpina takes two inputs: an \textsc{APn}, \ie a Petri Net (\textsc{Pn}) whose tokens are terms of an equational algebraic specification (\ie sorts, associated operations and equations), and whose behaviour is graphically defined; and a set of first-order formul\ae\xspace over the specification terms expressing invariants over the \textsc{Pn}. It allows the verification of such formul\ae\xspace by exhaustively exploring the \textsc{Pn} state space. If they are not satisfied, \Alpina returns a possible marking that violates the formul\ae.

In our context, \Alpina is used at each iteration step to check that new properties are satisfied. In case of a revision, the model-checker is run on each previously satisfied properties to ensure they are still satisfied by the revised model. 

%In \Alpina, \textsc{Pn}'s transitions can manipulate variable tokens graphically represented as transitions labels: \eg two transitions in \Fig \ref{fig:naivefs} are labeled with $\mathtt{[\$f]}$: it means each transition can consume a token of $\mathtt{\$f}$'s sort (here, the sort is $\mathtt{File}$, not visible in the \textsc{Pn}).

